Process Parameters (PP) and Global Variables (GV)'s possible usages are shown in the following table. The key difference is that Process Parameters can not be updated during the evaluation. This is a price to pay for efficient system exploration.

Note: Channel input variables behave similarly to process parameters within their valid scope. Local variables behave similarly to global variables within their valid scope.

2 PAT Type System

The input languages of PAT are weak typing (a.k.a. loose typing) languages and therefore no typing information is required when declaring a variable. The process parameters and channel input variables can take in values with different types at different time. As long as there is no type mismatch (e.g., integer is used as an array or Boolean), the execution will proceed. Otherwise, invalid type casting exception will be thrown.

The advantage claimed of weak typing is that it requires less effort on the part of the programmer than strong typing, because the compiler or interpreter implicitly performs certain kinds of conversions. However, one claimed disadvantage is that weakly typed programming systems catch fewer errors at compile time and some of these might still remain after testing has been completed.

3 No-Synchronization on Data Operations

This is a common problem raised by many users that, for the following program, can the two processes P() and Q() synchronise on the event a? If not, then how to make them synchronise on 'a' and preserve the execution of statement block ({x++}) in an atomic fashion?

Answer:

No-Synchronization on Data Operations is a design decision to void data race. If two data operations can synchronize, the update of the same global variable can lead to data race. Therefore, PAT will give a warning that if there one data operation and an event with same in different processes running in parallel.  

Back to the question, a intuitive solution is to put the event 'a' and increment statement in an atomic action as follows:

• P() = atomic{a -> update{x++} -> Skip};b -> Skip;
• Q() = a ->  c -> Skip;
• aSystem() = P() || Q();

Then x will be updated right after a is engaged, and a will be synchronised.

The other possible solution could be:

• P() = a -> update{x++} -> a1 -> b -> P();
• Q() = a -> a1 -> c -> P();

    4 Tips on using user defined data structures

Note that there is no difference between user defined types and normal variables (e.g. var x =1;). Only when the process parameter is used as user defined types, it is user's responsibility to make sure that the correct variable type is passed in since most of PAT modules don't have explicit types. See the example below.

#import "PAT.Lib.Set";
      var<Set> set1;
      Q() = P(set1);
      P(i) = initialize{i.Add(1);}-> ([i.GetSize() > 0] Skip);

Warning:

#import "PAT.Lib.Set";
      var<Set> set1;
      Q() = P(set1);
      P(i) = add1{i.Add(1);} -> Skip [] add2{i.Add(2);} -> Skip;

5 Tips on using string in LTL assertions.

PAT allows string in LTL assertions for complicated events like channel array events. However we don't do more refined parsing for the string. Therefore, we just compare the string with the event name. See the example below.